/*
 * SYmbolic Model-Based test case generation toOL for Real-Time systems (SYMBOLRT)
 * (C) Copyright 2010-2012 Federal University of Campina Grande (UFCG)
 * 
 * This file is part of SYMBOLRT.
 *
 * SYMBOLRT is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * SYMBOLRT is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with SYMBOLRT.  If not, see <http://www.gnu.org/licenses/>.
 * 
 * 
 * REVISION HISTORY:
 * Author                           Date           Brief Description
 * -------------------------------- -------------- ------------------------------
 * Wilkerson de Lucena Andrade      16/06/2011     An old class named TIOSTSPreprocessing (Version 1.2) was divided into two classes. This class only contains the completion algorithm (Version 1.0).
 *
 */
package br.edu.ufcg.symbolrt.algorithms;

import java.util.ArrayList;
import java.util.Collection;
import java.util.LinkedList;
import java.util.List;

import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.ClockGuard;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.SimpleClockGuard;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.Transition;
import br.edu.ufcg.symbolrt.exception.ClockGuardException;
import br.edu.ufcg.symbolrt.symbolicexecution.exception.IncompatibleOperationException;
import br.edu.ufcg.symbolrt.util.Constants;



public class CompositionCompletion {

	private static CompositionCompletion instance = null;


	private CompositionCompletion() {
	}

	/**
	 * Method used to obtain an instance of this class.
	 * @return An instance of {@link CompositionCompletion}.
	 */
	public static CompositionCompletion getInstance() {
		if (instance == null) {
			instance = new CompositionCompletion();
		}
		return instance;
	}
	
	public TIOSTS complete(TIOSTS tiosts) throws ClockGuardException, IncompatibleOperationException {
		TIOSTS tiostsComplete = tiosts.clone();
		tiostsComplete.setName(tiosts.getName() + "_complete");


		// Be compatible means not having don't care location.
		if (!isCompatible(tiosts)){
			throw new IncompatibleOperationException("The location 'don't care' must be ausent in TIOSTS location set.");
		}else{

			// Adding a don't care location to the tiosts
			Location dontCare = new Location(tiosts.getName()+"_Location");
			tiostsComplete.addLocation(dontCare);

			//Adding self-loops to the don't care location
			Collection<Action> totalActions = tiosts.getInputOutputActions();
			for(Action action : totalActions){
				tiostsComplete.createTransition(dontCare.getLabel(), Constants.GUARD_TRUE, Constants.GUARD_TRUE, action, null, null, Constants.DEADLINE_LAZY, dontCare.getLabel());
			}	
			
			//Despising the Start location
			Collection<Location> locations = tiosts.getLocations();
			locations.remove(tiosts.getInitialLocation());

			for (Location loc : locations) {
				//Including transitions with absent input actions
				if (!loc.getLabel().equals(dontCare.getLabel())){
					Collection<Action> absentInputActions = getRemainingInputActions(loc, tiosts.getInputActions());
					for (Action action : absentInputActions) {
						tiostsComplete.createTransition(loc.getLabel(), Constants.GUARD_TRUE, Constants.GUARD_TRUE, action, null, null, Constants.DEADLINE_LAZY, dontCare.getLabel());						
					}					
				
					//Including transitions with present input actions
					Collection<Action> presentInputActions = minusSet(tiosts.getInputActions(), absentInputActions);
				    Collection<Transition> currentTransitions = loc.getOutTransitions();
						
					for(Action presentAction : presentInputActions){
						String dataGuard = Constants.GUARD_TRUE;
						ClockGuard clockGuard = new ClockGuard();
						//boolean firstTime = true;
						for(Transition currentTransition:currentTransitions){
							if(presentAction.equals(currentTransition.getAction())){
								dataGuard = createDataGuard(currentTransition.getDataGuard(), dataGuard);
								// Because we don't afford clock guards with more than one constraint, the first guard initiation must be the assignment of the previous guards. 
								/*if(firstTime){
										clockGuard = currentTransition.getClockGuard();
										dataGuard = currentTransition.getDataGuard();
										firstTime = false;	
									
								}else{*/
									clockGuard = createClockGuard(currentTransition.getClockGuard(), clockGuard);
									dataGuard = createDataGuard(currentTransition.getDataGuard(), dataGuard);
								//}
							}
							
						}							
							//Negating data and clock guards
							dataGuard = Constants.GUARD_NEGATION + " (" + dataGuard + ")";
							//clockGuard = negateClockGuard(clockGuard); 
							tiostsComplete.createTransition(loc.getLabel(), dataGuard, clockGuard.toString(), presentAction, null, null, Constants.DEADLINE_LAZY, dontCare.getLabel());
					}				

				}

			}			
		}		
			return tiostsComplete;
	}
		
	/**
	 * Creates the clock guard of a transition considering the guard of specification and test purpose.
	 * @param specGuard The guard of a transition of specification.
	 * @param tpGuard The guard of a transition of test purpose.
	 * @return The clock guard resulting from conjunction of guards of specification and test purpose. 
	 */
	// TODO Refatorar depois. Deve ir para a classe ClockGuard
	private ClockGuard createClockGuard(ClockGuard specGuard, ClockGuard tpGuard){
		ClockGuard newClockGuard = new ClockGuard();
		
		for (SimpleClockGuard simpleClockGuard : specGuard.getClockGuard()) {
			newClockGuard.addSimpleClockGuard(simpleClockGuard.clone());
		}
		
		for (SimpleClockGuard simpleClockGuard : tpGuard.getClockGuard()) {
			newClockGuard.addSimpleClockGuard(simpleClockGuard.clone());
		}
		return newClockGuard;
	}
	
	
	/**
	 * Creates the data guard of a transition considering the guard of specification and test purpose.
	 * @param specGuard The guard of a transition of specification.
	 * @param tpGuard The guard of a transition of test purpose.
	 * @return The data guard resulting from conjunction of guards of specification and test purpose. 
	 */
	private String createDataGuard(String specGuard, String tpGuard){
		if (tpGuard == Constants.GUARD_TRUE) {
			return specGuard;
		} else if (specGuard == Constants.GUARD_TRUE){
			return tpGuard;
		} else {
			return specGuard + " " + Constants.GUARD_CONJUNCTION + " " + tpGuard;
		}
	}
	
	private Collection<Action> minusSet(Collection<Action> set1, Collection<Action> set2){
		Collection<Action> resultSet = new LinkedList<Action>();
		
		for(Action s:set1){
			if(!set2.contains(s)){
				resultSet.add(s);								
			}
		}
		return resultSet;		
	}
	
	/**
	 * Given all input actions of the model and a specific location, this method returns input actions that are not leaving the location. 
	 * @param loc The location to be analyzed. 
	 * @param inputActions All input actions present in the model.
	 * @return The remaining input actions that are not leaving loc.
	 */
	private Collection<Action> getRemainingInputActions(Location loc, Collection<Action> inputActions) { 
		Collection<Action> result = new ArrayList<Action>();
		Collection<Action> usedActions = loc.getOutActions();
		
		for (Action inputAction : inputActions) {
			if (!usedActions.contains(inputAction)){
				result.add(inputAction);
			}
		}
		
		return result;
	}
	
	
	/**
	 * Given a clock guard, this method returns its negation. It is assumed that the 
	 * parameter contains only one constraint of the form c#i where c is a clock, i is
	 * an integer constant, and # &isin; {<, <=, =>, >}. The symbol = is not allowed
	 * in the constraint because its negation is not supported in representation of zones.
	 * @param clockGuard The clock guard to negate.
	 * @return The negation of the clock guard.
	 * @throws ClockGuardException If the clock guard is not supported in test purposes.
	 */
	private ClockGuard negateClockGuard(ClockGuard clockGuard) throws ClockGuardException{
		ClockGuard newClockGuard = new ClockGuard();
		
		if (clockGuard.getClockGuard().size() != 1) {
			throw new ClockGuardException("Clock guards can have only one constraint. " + clockGuard.toString() + " "+ clockGuard.getClockGuard().size());
		}
		
		SimpleClockGuard simpleClockGuard = clockGuard.getClockGuard().get(0);
		
		if (simpleClockGuard.getRelation().equals(Constants.GUARD_EQUAL)) {
			throw new ClockGuardException("= is not allowed in clock guards of test purposes because its negation is not " +
					"supported in representation of zones.");
		}	
		
		String relation = "";
		
		if (simpleClockGuard.getRelation().equals(Constants.GUARD_LEQ)){
			relation = Constants.GUARD_GT;
		} else if (simpleClockGuard.getRelation().equals(Constants.GUARD_GEQ)){
			relation = Constants.GUARD_LT;
		} else if (simpleClockGuard.getRelation().equals(Constants.GUARD_LT)){
			relation = Constants.GUARD_GEQ;
		} else if (simpleClockGuard.getRelation().equals(Constants.GUARD_GT)){
			relation = Constants.GUARD_LEQ;
		} else {
			throw new ClockGuardException("The clock guard \"" + clockGuard.toString() + "\" is not supported in test purposes.");
		}

		/*if (clockGuard.indexOf(Constants.GUARD_LEQ) != -1) {
			return clockGuard.replaceFirst(Constants.GUARD_LEQ, Constants.GUARD_GT);
		} else if (clockGuard.indexOf(Constants.GUARD_GEQ) != -1) {
			return clockGuard.replaceFirst(Constants.GUARD_GEQ, Constants.GUARD_LT);
		} else if (clockGuard.indexOf(Constants.GUARD_LT) != -1) {
			return clockGuard.replaceFirst(Constants.GUARD_LT, Constants.GUARD_GEQ);
		} else if (clockGuard.indexOf(Constants.GUARD_GT) != -1) {
			return clockGuard.replaceFirst(Constants.GUARD_GT, Constants.GUARD_LEQ);
		} else {
			throw new ClockGuardException("The clock guard \"" + clockGuard + "\" is not supported in test purposes.");
		}*/
		
		
		SimpleClockGuard newSimpleClockGuard = new SimpleClockGuard(simpleClockGuard.getClockId(), simpleClockGuard.getClock(), relation, simpleClockGuard.getIntegerConstant());
		newClockGuard.addSimpleClockGuard(newSimpleClockGuard);
		
		return newClockGuard;
	}
	
	private boolean isCompatible(TIOSTS tiosts){
		boolean resp = true;
		
		for(Location loc:tiosts.getLocations()){
			if(loc.getLabel().equals(Constants.DONT_CARE_LOCATION)){
				resp = false;
			}
		}
		
		return resp;
		
	}

	
}
